COMMENT ⊗   VALID 00004 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	%ALGOL.SLI[F89,JMC]	Algol 48 and Algol 50
C00004 00003	Algol 48 version of the Algol 60 program
C00006 00004	Algol 50 version of the Algol 60 program
C00008 ENDMK
C⊗;
%ALGOL.SLI[F89,JMC]	Algol 48 and Algol 50
\input slide2.tex[1,jmc]
% gets rid of the vertical bars
\overfullrule=0pts
\bigskip
\centerline{ALGOL 48 AND ALGOL 50}
\bigskip
%
Algol 60 program for multiplication by addition
%
$$\vtop{\openup\jot\ialign{&$#$\hfil\cr
start:\quad &p := 0;\cr
	&i := n;\cr
loop: &{\bf if} i=0 {\bf then go to} done;\cr
	&p := p+m;\cr
	&i := i-1;\cr
	&{\bf go to} loop;\cr
done:\cr}}.$$
\bigskip
\noindent Correctness condition:
The program will eventually reach the label $done$ at which point
the variable $p$ will have the value $mn$.  This is conventionally
done using the inductive assertion method, attaching the assertion
$p=m(n-i)$ to the label $loop$.  It is shown that this property is
preserved in the loop.  One proves that the program terminates
by showing that the variable $i$ counts down from $n$ to $0$.
\vfill\eject
Algol 48 version of the Algol 60 program
%
$$\eqalign{p(t+1) = &{\bf if} pc(t) = 0 {\bf then} 0\cr
&{\bf else if} pc(t) = 3 {\bf then} p(t)+m\cr
&{\bf else} p(t)},$$
%
$$\eqalign{i(t+1) = &{\bf if} pc(t) = 1 {\bf then} n\cr
&{\bf else if} pc(t) = 4 {\bf then} i(t)-1\cr
&{\bf else} i(t)},$$
%
and
%
$$\eqalign{pc(t+1) = &{\bf if} pc(t) = 2 ∧ i(t)= 0 {\bf then} 6 \cr
&{\bf else if} pc(t) = 5 {\bf then} 2 \cr
&{\bf else} pc(t)+1}.$$
\medskip

	Its correctness is represented by the sentence
%
$$∀n(n≥0 ⊃ ∀t(pc(t) = 0 ⊃ ∃t'(t' > 0 ∧ pc(t') = 6 ∧ p(t') = mn))).$$
%
It may be proved from the sentences representing the
program supplemented by the axioms of arithmetic and the axiom
schema of mathematical induction.
Use mathematical induction on $n$
applied to a formula involving $p(t) = m(n-i(t))$.
\vfill\eject
Algol 50 version of the Algol 60 program

Preliminary axioms and definitions:
%
$$c(var,a(var,val,\xi)) = val,$$
%
$$var1 ≠ var2 ⊃ c(var2,a(var1,val,\xi)) = c(var2,\xi),$$
%
$$a(var,val2,a(var,val1,\xi)) = a(var,val2,\xi),$$
%
and
$$\eqalign{&var1 ≠ var2 ⊃ \cr
a(var2,val2,&a(var1,val1,\xi)) = a(var1,val1,a(var2,val2,\xi)).\cr}$$

	The following definitions

$$step(\xi) = a(pc,value(pc,\xi)+1,\xi),$$
%
$$goto(label,\xi) = a(pc,label,\xi).$$
shorten the expression of programs.  We mustn't forget to say $p≠i∧p≠pc∧i≠pc$.

%
$$\eqalign{∀t(\xi(t+1) = &{\bf if} c(pc,\xi(t)) = start\cr
&\quad{\bf then} step a(p,0,\xi(t))\cr
&{\bf else if} c(pc,\xi(t)) = start+1\cr
&\quad{\bf then} step a(i,n,\xi(t))\cr
&{\bf else if} c(pc,\xi(t)) = loop\cr
&\quad{\bf then} ({\bf if} c(i,\xi(t)) = 0 {\bf then} goto(done,\xi(t))\cr
&\quad{\bf else} step \xi(t))\cr
&{\bf else if} c(pc,\xi(t)) = loop + 1\cr
&\quad{\bf then} step a(p,c(p,\xi(t))+m,\xi(t))\cr
&{\bf else if} c(pc,\xi(t)) = loop +2\cr
&\quad{\bf then} step a(i,c(i,\xi(t))-1\xi(t))\cr
&{\bf else if} c(pc,\xi(t)) = loop +3\cr
&\quad{\bf then} goto(loop,\xi(t))\cr
&{\bf else} \xi(t+1))\cr}
$$
\vfill
\noindent {\fiverm algol.sli[f89,jmc]}
\vskip -1in
\end